$\forall$$A$:Type, $I$:MaInterface($A$), $i$:\{$i$:Id$\mid$ ($i$ $\in$ fpf{-}domain($I$))\} . \\[0ex]$I$($i$) \\[0ex]$\in$ (${\it ds}$:$x$:Id fp$\rightarrow$ Type $\times$ $k$:\{$k$:Knd$\mid$ $\uparrow$hasloc($k$;$i$)\} fp$\rightarrow$ $V$:Type $\times$ (State(${\it ds}$)$\rightarrow$$V$$\rightarrow$($A$ + Top)))